Nuprl Lemma : inc-fst_wf
11,40
postcript
pdf
p
:(
:
). inc-fst(
p
)
(
:
)
latex
Definitions
x
:
A
B
(
x
)
,
inc-fst(
p
)
,
<
a
,
b
>
,
n
+
m
,
,
,
{
x
:
A
|
B
(
x
)}
,
A
,
False
,
P
Q
,
x
:
A
B
(
x
)
,
void
,
a
<
b
,
A
B
,
x
:
A
.
B
(
x
)
,
#$n
,
t
T
Lemmas
le
wf
,
nat
wf
origin
p:(:
). inc-fst(p) 
(: ) p:(: ). inc-fst(p) (: ) B(x)
A
Q
B(x)
Bx:A. B(x) T